$\forall$$T$, ${\it T'}$:Type, $a$:$T$ List$^{+}$, $f$:($T$$\rightarrow$${\it T'}$). hd(map($f$;$a$)) $=$ $f$(hd($a$))